Nuprl Lemma : l_before_wf
11,40
postcript
pdf
T
:Type,
l
:(
T
List),
x
,
y
:
T
. l_before(
x
;
y
;
l
;
T
)
prop{i:l}
latex
Definitions
l_before(
x
;
y
;
l
;
T
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
sublist
wf
origin
T:Type, l:(T List), x,y:T. l_before(x; y; l; T) 
prop{i:l} T:Type, l:(T List), x,y:T. l_before(x; y; l; T) prop{i:l} Tx:A. B(x)